Theorem vtoclbg 3523

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-clel 2837

This theorem is used by:  alexeqg  3609  pm13.183  3624  elab6g  3627  elabgw  3635  sbc8g  3751  sbc2or  3752  sbccow  3766  sbcco  3769  sbc5ALT  3772  sbcie2g  3783  eqsbc1  3789  sbcng  3790  sbcimg  3791  sbcan  3792  sbcor  3793  sbcbig  3794  sbcal  3802  sbcex2  3803  sbcel1v  3808  sbcreu  3828  csbiebg  3884  sbcel12  4375  sbceqg  4376  csbie2df  4407  preq12bg  4817  elintrabg  4925  sbcbr123  5164  inisegn0  6099  fsn2g  7134  funfvima3  7234  elixpsn  8933  ixpsnf1o  8934  domeng  8957  rankcf  10768  kardeng  35578  eldm3  36261  elima4  36276  brsset  36387  brbigcup  36396  elfix2  36402  elfunsg  36414  elsingles  36416  funpartlem  36442  ellines  36652  elhf2g  36676  bj-elpwgALT  37718  cover2g  38395