Theorem vtoclbg 3524

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 347	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3522	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-clel 2837

This theorem is referenced by:  alexeqg  3610  pm13.183  3625  elab6g  3628  elabgw  3636  sbc8g  3752  sbc2or  3753  sbccow  3767  sbcco  3770  sbc5ALT  3773  sbcie2g  3784  eqsbc1  3790  sbcng  3791  sbcimg  3792  sbcan  3793  sbcor  3794  sbcbig  3795  sbcal  3803  sbcex2  3804  sbcel1v  3809  sbcreu  3829  csbiebg  3884  sbcel12  4365  sbceqg  4366  csbie2df  4397  preq12bg  4811  elintrabg  4919  sbcbr123  5154  inisegn0  6087  fsn2g  7120  funfvima3  7220  elixpsn  8919  ixpsnf1o  8920  domeng  8943  rankcf  10735  eldm3  36111  elima4  36126  brsset  36237  brbigcup  36246  elfix2  36252  elfunsg  36264  elsingles  36266  funpartlem  36292  ellines  36502  elhf2g  36526  bj-elpwgALT  37539  cover2g  38215