Theorem vtoclbg 3529

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-clel 2809

This theorem is referenced by:  alexeqg  3604  pm13.183  3621  elab6g  3624  sbc8g  3750  sbc2or  3751  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcie2g  3784  eqsbc1  3791  sbcng  3792  sbcimg  3793  sbcan  3794  sbcor  3795  sbcbig  3796  sbcal  3806  sbcex2  3807  sbcel1v  3813  sbcreu  3835  csbiebg  3891  sbcel12  4373  sbceqg  4374  csbie2df  4405  preq12bg  4816  elintrabg  4927  sbcbr123  5164  inisegn0  6055  fsn2g  7089  funfvima3  7191  elixpsn  8882  ixpsnf1o  8883  domeng  8909  1sdomOLD  9200  rankcf  10722  eldm3  34420  elima4  34436  brsset  34550  brbigcup  34559  elfix2  34565  elfunsg  34577  elsingles  34579  funpartlem  34603  ellines  34813  elhf2g  34837  bj-elpwgALT  35598  cover2g  36247  elabgw  40690  sbcrexgOLD  41166