Theorem vtoclbg 3298

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 334	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3297	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523   ∈ wcel 2030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233

This theorem is referenced by:  alexeqg  3363  pm13.183  3376  sbc8g  3476  sbc2or  3477  sbcco  3491  sbc5  3493  sbcie2g  3502  eqsbc3  3508  sbcng  3509  sbcimg  3510  sbcan  3511  sbcor  3512  sbcbig  3513  sbcal  3518  sbcex2  3519  sbcel1v  3528  sbcreu  3548  csbiebg  3589  sbcel12  4016  sbceqg  4017  elpwg  4199  snssgOLD  4349  preq12bg  4417  elintgOLD  4516  elintrabg  4521  sbcbr123  4739  opelresgOLD  5440  inisegn0  5532  funfvima3  6535  elixpsn  7989  ixpsnf1o  7990  domeng  8011  1sdom  8204  rankcf  9637  eldm3  31777  br1steqgOLD  31798  br2ndeqgOLD  31799  elima4  31803  brsset  32121  brbigcup  32130  elfix2  32136  elfunsg  32148  elsingles  32150  funpartlem  32174  ellines  32384  elhf2g  32408  cover2g  33639  sbcrexgOLD  37666  sbcangOLD  39056  sbcorgOLD  39057  sbcalgOLD  39069  sbcexgOLD  39070  sbcel12gOLD  39071  sbcel1gvOLD  39408